Termination Proof Script
Consider the TRS R consisting of the rewrite rule
1:
f
(
g
(
f
(
a
),
h
(
a
,
f
(
a
))))
→
f
(
h
(
g
(
f
(
a
),
a
),
g
(
f
(
a
),
f
(
a
))))
There is one dependency pair:
2:
F
(
g
(
f
(
a
),
h
(
a
,
f
(
a
))))
→
F
(
h
(
g
(
f
(
a
),
a
),
g
(
f
(
a
),
f
(
a
))))
The approximated dependency graph contains no SCCs and hence the TRS is trivially terminating.
Tyrolean Termination Tool
(0.01 seconds) --- May 3, 2006